COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.require "memo.pub[let,jmc]" source
C00012 ENDMK
C⊗;
.require "memo.pub[let,jmc]" source;
.once center
%3CORRECTNESS OF %2samefringe%1


	We make the following LISP definitions:

!!z1:	%2fringe x ← qif qat x qthen <x> qelse fringe qa x * fringe qd x%1,

where %2u_*_v%1 denotes %2append[u,v]%1 and satisfies

!!z1a:	%2u * v ← qif qn u qthen v qelse qa u . [qd u * v]%1,

!!z2:	%2samefringe[x,y] ← x qeq y ∨ [¬qat x ∧ ¬qat y ∧
same[gopher x, gopher y]%1,

!!z3:	%2same[x,y] ← qa x qeq qa y ∧ samefringe[qd x, qd y]%1,

and

!!z4:	%2gopher x ← qif qat qa x qthen x qelse gopher[qaa x . [qda x . qd x]]%1.

	%2fringe x%1, which was called %2flatten x%1
in the %2Course Notes%1, gives a list
of the atoms in the S-expression %2x%1.  Thus %2fringe%1[((A.B).C)]_=_(A_B_C).
We also have %2fringe%1[(A.(B.C))]_=_(A_B_C), so that different S-expressions
can have the same fringe.  Indeed our object is to prove

%3Theorem 1%1 - %2∀x y.(samefringe[x,y] ≡ fringe x = fringe y%1).

	%2samefringe%1 and %2same%1 are mutually recursive LISP predicates,
and %2gopher%1 is an auxiliary function that digs out the first atom
of an S-expression piling whatever else it meets onto the %2cdr%1 part
of the expression.  Thus %2gopher%1[(((A.B).(C.D)).(E.F))]_=_(A.(B.((C.D).(E.F)))).

	The proof is divided into five parts.  First we convert the recursive
programs into first order logic functional equations.  %2fringe%1 and %2gopher%1
convert easily, but since %2samefringe%1 and %1same%1 are predicates, they
must be expressed in terms of pseudo-predicates %2samefringea%1 and %2samea%1
which have functional equations using the pseudo-propositional connnectives.

	Next we prove that %2fringe%1 and %2gopher%1 are total and prove
some lemmas about their properties.  These proofs are straightforward
structural inductions.

	Next we prove that that %2samefringea%1 is total.  The proof is
a course-of-values induction on %2size_x_+_size_y%1.

	From this we show that the predicates %2samefringe%1 and %2same%1
satisfy their recursion equations using genuine propositional connectives.

	Finally, we show that the predicate %2fringe x = fringe y%1 satisfies
the functional equation of %2samefringe[x,y]%1.  Since %2samefringe%1 has
been proved total, this allows use to use the minimization schema of
%2samefringe%1 to conclude the theorem.


Part 1

	Equations ({eq z1}) to ({eq z4}) become

!!z5:	%2∀x.[fringe x = qif qat x qthen <x> qelse fringe qa x * fringe qd x]%1,

!!z6:	%2∀u v.[u * v = qif qn u qthen v qelse qa u . [qd u * v]]%1,

!!z7:	%2∀x y.[samefringe[x,y] ≡ [samefringea[x,y] = T]]%1,

!!z8:	%2∀x y.[samefringea[x,y] = [x = y] or [not aatom x and not aatom y
and samea[gopher x, gopher y]]%1,

!!z9:	%2∀x y.[same[x,y] ≡ [samea[x,y] = T]]%1,

!!z10:	%2∀x y.[samea[x,y] = [qa x = qa y] and samefringe[qd x, qd y]]%1,

and

!!z11:	%2∀x.[gopher x = qif qat qa x qthen x qelse
gopher[qaa x.[qda x . qd x]]]%1.

	Notice that the recursively defined predicates %2samefringe%1
and %2same%1 must be defined in terms of the pseudo-predicates
%2samefringea%1 and %2same%1 in order to legitimately translate
the recursion equations into first order formulas.


%3Lemmas about %2gopher%1.

	The first lemma is that %2gopher%1 is total provided its
argument is not atomic.  Since every non-atom is the result of a %2cons%1,
we can express this assertion in the form

Lemma 1: %2∀x y.(issexp gopher[x.y])%1.

It is proved by simple S-expression induction on the sentence

!!z13:	%2qF[x] ≡ ∀y.issexp gopher[x.y]%1,

The general induction statement

!!z14:	∀x.(qat x ⊃ qF[x]) ∧ ∀x.(¬qat x ∧ qF[qa x] ∧ qF[qd x] ⊃ qF[x])
⊃ ∀x.qF[x]%1

then takes the form

!!z15:	%2∀x.(qat x ⊃ ∀y.issexp gopher[x.y]) ∧ ∀x.(¬qat x ∧ ∀y.issexp
gopher[qa x . y] ∧ ∀y.issexp gopher[qd x . y] ⊃ ∀y.issexp gopher[x.y])
⊃ ∀x ∀y.issexp gopher[x.y]%1.

The conclusion of ({eq z15}) is our goal.  Therefore we must establish
its premisses.  Each of the two premisses is an implication
universally quantified on %2x%1 with
%2∀y.issexp gopher[x.y]%1 as a conclusion but with different premisses.
Thus we must establish %2∀y.issexp gopher[x.y]%1 under the hypothesis
%2qat x%1 and again under the hypothesis %2¬qat_x ∧_∀y.issexp_gopher[qa_x_._y]
∧_∀y.issexp_gopher[qd_x_._y]%1.  In the atomic case we compute as follows:

!!z16:	%2issexp gopher[x.y] ≡ issexp[qif qat qa [x.y] qthen x.y qelse
gopher[qaa[x.y].[qda[x.y].qd[x.y]]]

	≡ qif qat x qthen issexp[x.y] qelse issexp gopher[qa x.[qd x. y]]

	≡ issexp[x.y]

	≡ %3true%1.

The first equivalence is established by substituting %2x.y%1 for %2x%1 in
({eq z11}), the first order characterization of %2gopher%1.  The second
follows by distributing the predicate %2issexp%1 into the conditional
expression and some simplification based on the algebraic relations among
the LISP functions.  Next we use the fact that %2x%1 is assumed atomic,
and finally we use axiom L8 asserting that the %2cons%1 of two S-expressions
is an S-expression.  Since %2y%1 was not subjected to any conditions, we
are entitled to write %2∀y.issexp gopher[x.y]%1 and then to discharge assumption
that %2x%1 is atomic getting  %2qat_x_⊃_∀y.issexp_gopher[x.y]%1, and since
%2x%1 wasn't subjected to conditions, we can finally write

!!z17:	%2∀x.(qat x ⊃ ∀y.issexp gopher[x.y])%1.

	The non-atomic case is similar.  The first steps are as before
but we continue differently.  Thus

%2issexp gopher[x.y] ≡ qif qat x qthen issexp[x.y] qelse issexp gopher[qa x.
[qd x . y]]

	≡ issexp gopher[qa x.[qd x.y]]

	≡ %3true%1,

where the last step is justified by the induction hypothesis.  The steps
that introduce the implication signs and quantify are the same as in the
atomic case, so that

!!z18:	%2∀x.(¬qat x ∧ ∀y.issexp gopher[qa x, y] ∧ ∀y.issexp gopher[qd x,y]
⊃ ∀y.issexp gopher[x.y])%1

from which Lemma 1 follows.

Lemma 2: %2∀x y. ¬qat gopher[x.y] ∧ qat qa gopher[x.y]%1.

Proof: